翻訳と辞書 Words near each other ・ Existential clause ・ Existential counselling ・ Existential crisis ・ Existential fallacy ・ Existential generalization ・ Existential graph ・ Existential humanism ・ Existential instantiation ・ Existential migration ・ Existential nihilism ・ Existential phenomenology ・ Existential Psychotherapy ・ Existential Psychotherapy (book) ・ Existential quantification ・ Existential risk from artificial general intelligence ・ Existential theory of the reals ・ Existential therapy ・ Existentialism ・ Existentialism and Humanism ・ Existentialist anarchism ・ Existentially closed model ・ Existentiell ・ Existenz ・ Existenz (disambiguation) ・ Existenz (journal) ・ Exister ・ Existere ・ Existing visitor optimisation ・ Existir ・ Exists (band) Dictionary Lists mini英和辞書 mini和英辞書 Webster 1913 Latin-English FOLDOC Wikipedia English ウィキペディア

翻訳と辞書　辞書検索 [ 開発暫定版 ] スポンサード リンク Existential theory of the reals ： ウィキペディア英語版 Existential theory of the reals In mathematical logic, computational complexity theory, and computer science, the existential theory of the reals is the set of all true sentences of the form : $\backslash exists\; X\_1\; \backslash cdots\; \backslash exists\; X\_n\; \backslash ,\; F(X\_1,\backslash dots,\; X\_n),\; \backslash ,$ where $F(X\_1,\backslash dots\; X\_n)$ is a quantifier-free formula involving equalities and inequalities of real polynomials.〔.〕 The decision problem for the existential theory of the reals is the problem of finding an algorithm that decides, for each such formula, whether it is true or false. Equivalently, it is the problem of testing whether a given semialgebraic set is non-empty.〔 This decision problem is NP-hard and lies in PSPACE.〔.〕 Thus it has significantly lower complexity than Alfred Tarski's quantifier elimination procedure for deciding statements in the first-order theory of the reals without the restriction to existential quantifiers.〔 However, in practice, general methods for the first-order theory remain the preferred choice for solving these problems.〔 Many natural problems in geometric graph theory, especially problems of recognizing geometric intersection graphs and straightening the edges of graph drawings with crossings, may be solved by translating them into instances of the existential theory of the reals, and are complete for this theory. The complexity class $\backslash exists\backslash mathbb$, which lies between NP and PSPACE, has been defined to describe this class of problems.〔 ==Background== In mathematical logic, a theory is a formal language consisting of a set of sentences written using a fixed set of symbols. The first-order theory of real closed fields has the following symbols:〔 *the constants 0 and 1, *a countable collection of variables $X\_i$, *the addition, subtraction, multiplication, and (optionally) division operations, *symbols <, ≤, =, ≥, >, and ≠ for comparisons of real values, *the logical connectives ∧, ∨, ¬, and ⇔, *parentheses, and *the universal quantifier ∀ and the existential quantifier ∃ A sequence of these symbols forms a sentence that belongs to the first-order theory of the reals if it is grammatically well formed, all its variables are properly quantified, and (when interpreted as a mathematical statement about the real numbers) it is a true statement. As Tarski showed, this theory can be described by an axiom schema and a decision procedure that is complete and effective: for every fully quantified and grammatical sentence, either the sentence or its negation (but not both) can be derived from the axioms. The same theory describes every real closed field, not just the real numbers.〔 However, there are other number systems that are not accurately described by these axioms; in particular, the theory defined in the same way for integers instead of real numbers is undecidable, even for existential sentences (Diophantine equations) by Matiyasevich's theorem.〔〔.〕 The existential theory of the reals is the subset of the first-order theory consisting of sentences in which all the quantifiers are existential and they appear before any of the other symbols. That is, it is the set of all true sentences of the form : $\backslash exists\; X\_1\; \backslash cdots\; \backslash exists\; X\_n\; \backslash ,\; F(X\_1,\backslash dots,\; X\_n),\; \backslash ,$ where $F(X\_1,\backslash dots\; X\_n)$ is a quantifier-free formula involving equalities and inequalities of real polynomials. The decision problem for the existential theory of the reals is the algorithmic problem of testing whether a given sentence belongs to this theory; equivalently, for strings that pass the basic syntactical checks (it uses the correct symbols with the correct syntax, and has no unquantified variables) it is the problem of testing whether the sentence is a true statement about the real numbers. The set of ''n''-tuples of real numbers $(X\_1,\backslash dots\; X\_n)$ for which $F(X\_1,\backslash dots\; X\_n)$ is true is called a semialgebraic set, so the decision problem for the existential theory of the reals can equivalently be rephrased as testing whether a given semialgebraic set is nonempty.〔 In determining the time complexity of algorithms for the decision problem for the existential theory of the reals, it is important to have a measure of the size of the input. The simplest measure of this type is the length of a sentence: that is, the number of symbols it contains.〔 However, in order to achieve a more precise analysis of the behavior of algorithms for this problem, it is convenient to break down the input size into several variables, separating out the number of variables to be quantified, the number of polynomials within the sentence, and the degree of these polynomials.〔 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Existential theory of the reals」の詳細全文を読む スポンサード リンク 翻訳と辞書 : 翻訳のためのインターネットリソース Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.